| Definitions | A & B, x:A B(x), P & Q, FairFifo, Id, vartype(i;x), M(i), M.ds(x), x:A  B(x),  x:A. B(x), Action(i),  b,  A, valtype(i;a), M.da(a), P   Q, IdLnk, w.M, f(a), M.init(x,v),  , M.pre(a,s,v), M.ef(k,x,s,v,w), M.send(k;l;s;v;ms;i), M.frame(k affects x), s = t, M.sframe(k sends <l,tg>), Msg, type List, A B, unsolvable M.pre(a,s), a declared in M, left+right, P  Q, Knd,  x:A. B(x), M.aframe(k affects x), M.rframe(k reads x), w-machine-independent(w;i;k;x), M.bframe(k sends on l), PossibleWorld(D;w), Dsys, t  T, D1  D2, World, M1 M2, isnull(a), kind(a), rcv(l,tg), source(l), #$n, a<b, Void, False, {x:A| B(x) },  , s(i;t).x,  x.A(x),  x. t(x), a(i;t), State(ds), n+m, M.state, islocal(k), val(a), act(k), locl(a), Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi, z != f(x) P(a;z), s ~ t, True, m(i;t), withlnk(l;mss), Type, Top,  x:A. B(x), S T, Prop, b,  , a = b, P  Q, Unit, mlnk(m), Msg(M), Dec(P), {T} |
| Lemmas | ma-bframe wf, ma-bframe-sub, ma-rframe wf, ma-rframe-sub, ma-aframe wf, ma-aframe-sub, ma-npre-sub, ma-decla-sub, ma-decla wf2, decidable ma-decla, ma-npre wf, ma-sframe wf, ma-sframe-sub, ma-frame-sub, ma-frame wf, w-withlnk wf, w-m wf, w-Msg wf, Msg wf, mlnk wf, ifthenelse wf, top wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, ma-send-sub, ma-ef-sub, Knd wf, false wf, true wf, locl wf, ma-pre-sub, actof wf, w-val wf, islocal wf, nat properties, nat wf, w-a wf, ma-init-sub, subtype rel self, w-s wf, le wf, IdLnk wf, w-M wf, rcv wf, lsrc wf, not wf, assert wf, w-isnull wf, w-action wf, w-valtype wf, ma-da wf, ma-da-sub, w-kind wf, Id wf, subtype rel transitivity, w-vartype wf, ma-ds wf, ma-ds-sub, d-m wf, possible-world wf, world wf, d-sub wf, dsys wf |